#!/usr/bin/env ruby

class String
    def begins?(s)
        self[0...(s.size)] == s
    end

    def ends?(s)
        self[(self.size - s.size)...(self.size)] == s
    end
end

REGULAR_ARGS = 2
BMC_ARGS = 4

STATES_EXTRACTOR = /number of reachable states = ([0-9\.e\+]+)/
MEMORY_EXTRACTOR = /BDD memory in use = ([0-9\.e\+]+)/
COUNT_EXTRACTOR = /([0-9\.e\+]+)/
NUMBER_EXTRACTOR = /([0-9\.]+)/

MCMAS_EXECUTABLE = "mcmas"

INPUT_FOLDER = "TGC_Gen/"

if __FILE__ == $0 then

count = 3
max = 12
iterations = 3
increment = max / (iterations+1)

output = "data.csv"
contents = "File, Regular States, Regular Memory, Regular Time, BMC States, BMC Memory, BMC Time"
File.open(output, "w") do |handle|
       handle.puts contents

puts contents

Dir.foreach(INPUT_FOLDER) do |file|

    if file.begins?(".") or not file.ends?(".ispl") then
        #puts "The file #{file} is not a ISPL file and has been ignored."
        next
    end

    regulartime = Time.now

    output = `./#{MCMAS_EXECUTABLE} -e #{REGULAR_ARGS} #{INPUT_FOLDER}#{file}`

    regulartime = Time.now - regulartime

    regularstates = COUNT_EXTRACTOR.match(STATES_EXTRACTOR.match(output)[1])[1]
    a = regularstates.split("e+")[0].to_f
    b = regularstates.split("e+")[1].to_f
    regularstates = a * (10 ** b)
    regularmemory = COUNT_EXTRACTOR.match(MEMORY_EXTRACTOR.match(output)[1])[1].to_f

    bmctime = Time.now

    output = `./#{MCMAS_EXECUTABLE} -e #{BMC_ARGS} #{INPUT_FOLDER}#{file}`

    bmctime = Time.now - bmctime

    bmcstates = COUNT_EXTRACTOR.match(STATES_EXTRACTOR.match(output)[1])[1]
    a = bmcstates.split("e+")[0].to_f
    b = bmcstates.split("e+")[1].to_f
    bmcstates = a * (10 ** b)
    bmcmemory = COUNT_EXTRACTOR.match(MEMORY_EXTRACTOR.match(output)[1])[1].to_f
    
    contents = "#{file}, #{regularstates}, #{regularmemory}, #{regulartime}, #{bmcstates}, #{bmcmemory}, #{bmctime}, #{(bmcstates - regularstates) / regularstates}, #{(bmcmemory - regularmemory) / regularmemory}, #{(bmctime - regulartime) / regulartime}"
    
    #File.open(output, "a") do |handle|
       handle.puts contents
    #end

    puts contents
end
end

=begin
file = "small.ispl"

depthcounter = increment

for i in 1..iterations
    regulartime = Time.now

    output = `./#{MCMAS_EXECUTABLE} -e #{REGULAR_ARGS} #{file}`

    regulartime = Time.now - regulartime

    regularstates = COUNT_EXTRACTOR.match(STATES_EXTRACTOR.match(output)[1])
    regularmemory = COUNT_EXTRACTOR.match(MEMORY_EXTRACTOR.match(output)[1])

    bmctime = Time.now

    output = `./#{MCMAS_EXECUTABLE} -e #{BMC_ARGS} #{file}`

    bmctime = Time.now - bmctime

    bmcstates = COUNT_EXTRACTOR.match(STATES_EXTRACTOR.match(output)[1])
    bmcmemory = COUNT_EXTRACTOR.match(MEMORY_EXTRACTOR.match(output)[1])
    puts depthcounter
    #puts "#{count}, #{max}, asd, #{file}, #{regularstates}, #{regularmemory}, #{regulartime}, #{bmcstates}, #{bmcmemory}, #{bmctime}"

    depthcounter += increment

end
=end

end
